ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List),
a:((k:{k:Knd| (k  ks)} decl-state(ds)ma-valtype(da; k)T)), snd:msg-spec(ds; da),
l:IdLnk.
((fpf-dom(id-deq; x; ds)))
 (ecl-m3(a; snd; x; l)
 ( k:{k:Knd| (k  ks)} (tg:{tg:Id| (tg  ecl-tags(l; snd))} 
 (  (decl-state(fpf-join(id-deq; ds; fpf-single(x; T)))ma-valtype(da; k)
 (  (fpf-cap(da; Kind-deq; rcv(l,tg); void) List))) List) 

latex

Definitions

t  T, x:A. B(x), P  Q, False, A, A  B, , isect(A; x.B(x)), top, id-deq, fpf-single(x; v), b, b, , prop{i:l}, Type, x.A(x), x. t(x), fpf(A; a.B(a)), fpf-dom(eq; x; f), P  Q, P  Q, Unit, left + right, fpf-join(eq; f; g), f(a), atom{$n:n}, msg-spec(ds; da), x:A. B(x), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , spreadn(a; x,y,z.t(x;y;z)), map(f; as), let x = a in b(x), ecl-m3(a; snd; x; l), [], <a, b>, idlnk-deq, Kind-deq, IdLnk, Knd, product-deq(A; B; a; b), fpf-cap(f; eq; x; z), void, rcv(l,tg), type List, ma-valtype(da; k), x:AB(x), decl-state(ds), , x:A  B(x), Id, ecl-tags(l; snd), (x  l), {x:A| B(x)} , s = t, ||as||, fpf-ap(f; eq; x), A c B, a < b, EqDecider(T), sqequal(s; t), guard(T), sq_type(T), l_all(L; T; x.P(x)), t.2, t.1, msg-item(ds; da; k; l), P  Q, subtype(S; T)

Lemmas

subtype rel list, l member subtype, member-ecl-tags, list-set-type2, pi2 wf, pi1 wf, msg-item wf, product-deq wf, idlnk-deq wf, deq wf, IdLnk wf, msg-spec wf, fpf wf, let wf, map wf, nat wf, ecl-tags wf, ifthenelse wf, l member wf, ma-valtype wf, Knd wf, Kind-deq wf, rcv wf, nat properties, decl-state wf, subtype rel dep function, fpf-join wf, fpf-cap wf, fpf-cap-join-subtype, fpf-join-cap-sq, fpf-single wf, top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf, fpf-cap-single1, Id wf, id-deq wf, subtype rel self